H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.157 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule List

((isSuffixOf :: [()] -> [()] -> Bool) :: [()] -> [()] -> Bool)

module List where

import qualified Maybe
import qualified Prelude

isPrefixOf :: Eq a => [a] -> [a] -> Bool

isPrefixOf	[] _	=	True
isPrefixOf	_ []	=	False
isPrefixOf	(x : xs) (y : ys)	=	x == y && isPrefixOf xs ys

isSuffixOf :: Eq a => [a] -> [a] -> Bool

isSuffixOf

x y

reverse x `isPrefixOf` reverse y

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule List

((isSuffixOf :: [()] -> [()] -> Bool) :: [()] -> [()] -> Bool)

module List where

import qualified Maybe
import qualified Prelude

isPrefixOf :: Eq a => [a] -> [a] -> Bool

isPrefixOf	[] vw	=	True
isPrefixOf	vx []	=	False
isPrefixOf	(x : xs) (y : ys)	=	x == y && isPrefixOf xs ys

isSuffixOf :: Eq a => [a] -> [a] -> Bool

isSuffixOf

x y

reverse x `isPrefixOf` reverse y

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

mainModule List

(isSuffixOf :: [()] -> [()] -> Bool)

module List where

import qualified Maybe
import qualified Prelude

isPrefixOf :: Eq a => [a] -> [a] -> Bool

isPrefixOf	[] vw	=	True
isPrefixOf	vx []	=	False
isPrefixOf	(x : xs) (y : ys)	=	x == y && isPrefixOf xs ys

isSuffixOf :: Eq a => [a] -> [a] -> Bool

isSuffixOf

x y

reverse x `isPrefixOf` reverse y

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="isSuffixOf",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="isSuffixOf wu3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="isSuffixOf wu3 wu4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="isPrefixOf (reverse wu3) (reverse wu4)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="isPrefixOf (foldl (flip (:)) [] wu3) (reverse wu4)",fontsize=16,color="burlywood",shape="box"];391[label="wu3/wu30 : wu31",fontsize=10,color="white",style="solid",shape="box"];6 -> 391[label="",style="solid", color="burlywood", weight=9];
391 -> 7[label="",style="solid", color="burlywood", weight=3];
392[label="wu3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 392[label="",style="solid", color="burlywood", weight=9];
392 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="isPrefixOf (foldl (flip (:)) [] (wu30 : wu31)) (reverse wu4)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="isPrefixOf (foldl (flip (:)) [] []) (reverse wu4)",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9 -> 234[label="",style="dashed", color="red", weight=0];
9[label="isPrefixOf (foldl (flip (:)) (flip (:) [] wu30) wu31) (reverse wu4)",fontsize=16,color="magenta"];9 -> 235[label="",style="dashed", color="magenta", weight=3];
9 -> 236[label="",style="dashed", color="magenta", weight=3];
9 -> 237[label="",style="dashed", color="magenta", weight=3];
9 -> 238[label="",style="dashed", color="magenta", weight=3];
10[label="isPrefixOf [] (reverse wu4)",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
235[label="[]",fontsize=16,color="green",shape="box"];236[label="wu4",fontsize=16,color="green",shape="box"];237[label="wu30",fontsize=16,color="green",shape="box"];238[label="wu31",fontsize=16,color="green",shape="box"];234[label="isPrefixOf (foldl (flip (:)) (flip (:) wu15 wu16) wu17) (reverse wu18)\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];394[label="wu17/wu170 : wu171",fontsize=10,color="white",style="solid",shape="box"];234 -> 394[label="",style="solid", color="burlywood", weight=9];
394 -> 271[label="",style="solid", color="burlywood", weight=3];
395[label="wu17/[]",fontsize=10,color="white",style="solid",shape="box"];234 -> 395[label="",style="solid", color="burlywood", weight=9];
395 -> 272[label="",style="solid", color="burlywood", weight=3];
13[label="True",fontsize=16,color="green",shape="box"];271[label="isPrefixOf (foldl (flip (:)) (flip (:) wu15 wu16) (wu170 : wu171)) (reverse wu18)\n  Eq a",fontsize=16,color="black",shape="box"];271 -> 273[label="",style="solid", color="black", weight=3];
272[label="isPrefixOf (foldl (flip (:)) (flip (:) wu15 wu16) []) (reverse wu18)\n  Eq a",fontsize=16,color="black",shape="box"];272 -> 274[label="",style="solid", color="black", weight=3];
273 -> 234[label="",style="dashed", color="red", weight=0];
273[label="isPrefixOf (foldl (flip (:)) (flip (:) (flip (:) wu15 wu16) wu170) wu171) (reverse wu18)\n  Eq a",fontsize=16,color="magenta"];273 -> 275[label="",style="dashed", color="magenta", weight=3];
273 -> 276[label="",style="dashed", color="magenta", weight=3];
273 -> 277[label="",style="dashed", color="magenta", weight=3];
274[label="isPrefixOf (flip (:) wu15 wu16) (reverse wu18)\n  Eq a",fontsize=16,color="black",shape="box"];274 -> 278[label="",style="solid", color="black", weight=3];
275[label="flip (:) wu15 wu16\n  Eq a",fontsize=16,color="black",shape="triangle"];275 -> 279[label="",style="solid", color="black", weight=3];
276[label="wu170\n  Eq a",fontsize=16,color="green",shape="box"];277[label="wu171\n  Eq a",fontsize=16,color="green",shape="box"];278[label="isPrefixOf ((:) wu16 wu15) (reverse wu18)\n  Eq a",fontsize=16,color="black",shape="box"];278 -> 280[label="",style="solid", color="black", weight=3];
279[label="(:) wu16 wu15\n  Eq a",fontsize=16,color="green",shape="box"];280 -> 285[label="",style="dashed", color="red", weight=0];
280[label="isPrefixOf ((:) wu16 wu15) (foldl (flip (:)) [] wu18)\n  Eq a",fontsize=16,color="magenta"];280 -> 286[label="",style="dashed", color="magenta", weight=3];
280 -> 287[label="",style="dashed", color="magenta", weight=3];
286[label="[]\n  Eq a",fontsize=16,color="green",shape="box"];287[label="wu18\n  Eq a",fontsize=16,color="green",shape="box"];285[label="isPrefixOf ((:) wu16 wu15) (foldl (flip (:)) wu19 wu181)\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];398[label="wu181/wu1810 : wu1811",fontsize=10,color="white",style="solid",shape="box"];285 -> 398[label="",style="solid", color="burlywood", weight=9];
398 -> 289[label="",style="solid", color="burlywood", weight=3];
399[label="wu181/[]",fontsize=10,color="white",style="solid",shape="box"];285 -> 399[label="",style="solid", color="burlywood", weight=9];
399 -> 290[label="",style="solid", color="burlywood", weight=3];
289[label="isPrefixOf ((:) wu16 wu15) (foldl (flip (:)) wu19 (wu1810 : wu1811))\n  Eq a",fontsize=16,color="black",shape="box"];289 -> 291[label="",style="solid", color="black", weight=3];
290[label="isPrefixOf ((:) wu16 wu15) (foldl (flip (:)) wu19 [])\n  Eq a",fontsize=16,color="black",shape="box"];290 -> 292[label="",style="solid", color="black", weight=3];
291 -> 285[label="",style="dashed", color="red", weight=0];
291[label="isPrefixOf ((:) wu16 wu15) (foldl (flip (:)) (flip (:) wu19 wu1810) wu1811)\n  Eq a",fontsize=16,color="magenta"];291 -> 293[label="",style="dashed", color="magenta", weight=3];
291 -> 294[label="",style="dashed", color="magenta", weight=3];
292[label="isPrefixOf ((:) wu16 wu15) wu19\n  Eq a",fontsize=16,color="burlywood",shape="box"];401[label="wu19/wu190 : wu191",fontsize=10,color="white",style="solid",shape="box"];292 -> 401[label="",style="solid", color="burlywood", weight=9];
401 -> 295[label="",style="solid", color="burlywood", weight=3];
402[label="wu19/[]",fontsize=10,color="white",style="solid",shape="box"];292 -> 402[label="",style="solid", color="burlywood", weight=9];
402 -> 296[label="",style="solid", color="burlywood", weight=3];
293 -> 275[label="",style="dashed", color="red", weight=0];
293[label="flip (:) wu19 wu1810\n  Eq a",fontsize=16,color="magenta"];293 -> 297[label="",style="dashed", color="magenta", weight=3];
293 -> 298[label="",style="dashed", color="magenta", weight=3];
294[label="wu1811\n  Eq a",fontsize=16,color="green",shape="box"];295[label="isPrefixOf ((:) wu16 wu15) (wu190 : wu191)\n  Eq a",fontsize=16,color="black",shape="box"];295 -> 299[label="",style="solid", color="black", weight=3];
296[label="isPrefixOf ((:) wu16 wu15) []\n  Eq a",fontsize=16,color="black",shape="box"];296 -> 300[label="",style="solid", color="black", weight=3];
297[label="wu19\n  Eq a",fontsize=16,color="green",shape="box"];298[label="wu1810\n  Eq a",fontsize=16,color="green",shape="box"];299 -> 301[label="",style="dashed", color="red", weight=0];
299[label="wu16 == wu190 && isPrefixOf wu15 wu191\n  Eq a",fontsize=16,color="magenta"];299 -> 302[label="",style="dashed", color="magenta", weight=3];
299 -> 303[label="",style="dashed", color="magenta", weight=3];
299 -> 304[label="",style="dashed", color="magenta", weight=3];
300[label="False",fontsize=16,color="green",shape="box"];302[label="wu16 == wu190\n  Eq a",fontsize=16,color="blue",shape="box"];405[label="== :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 405[label="",style="solid", color="blue", weight=9];
405 -> 305[label="",style="solid", color="blue", weight=3];
406[label="== :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 406[label="",style="solid", color="blue", weight=9];
406 -> 306[label="",style="solid", color="blue", weight=3];
407[label="== :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 407[label="",style="solid", color="blue", weight=9];
407 -> 307[label="",style="solid", color="blue", weight=3];
408[label="== :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 408[label="",style="solid", color="blue", weight=9];
408 -> 308[label="",style="solid", color="blue", weight=3];
409[label="== :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 409[label="",style="solid", color="blue", weight=9];
409 -> 309[label="",style="solid", color="blue", weight=3];
410[label="== :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 410[label="",style="solid", color="blue", weight=9];
410 -> 310[label="",style="solid", color="blue", weight=3];
411[label="== :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 411[label="",style="solid", color="blue", weight=9];
411 -> 311[label="",style="solid", color="blue", weight=3];
412[label="== :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 412[label="",style="solid", color="blue", weight=9];
412 -> 312[label="",style="solid", color="blue", weight=3];
413[label="== :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 413[label="",style="solid", color="blue", weight=9];
413 -> 313[label="",style="solid", color="blue", weight=3];
414[label="== :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 414[label="",style="solid", color="blue", weight=9];
414 -> 314[label="",style="solid", color="blue", weight=3];
415[label="== :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 415[label="",style="solid", color="blue", weight=9];
415 -> 315[label="",style="solid", color="blue", weight=3];
416[label="== :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 416[label="",style="solid", color="blue", weight=9];
416 -> 316[label="",style="solid", color="blue", weight=3];
417[label="== :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 417[label="",style="solid", color="blue", weight=9];
417 -> 317[label="",style="solid", color="blue", weight=3];
418[label="== :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];302 -> 418[label="",style="solid", color="blue", weight=9];
418 -> 318[label="",style="solid", color="blue", weight=3];
303[label="wu191\n  Eq a",fontsize=16,color="green",shape="box"];304[label="wu15\n  Eq a",fontsize=16,color="green",shape="box"];301[label="wu24 && isPrefixOf wu25 wu26\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];419[label="wu24/False",fontsize=10,color="white",style="solid",shape="box"];301 -> 419[label="",style="solid", color="burlywood", weight=9];
419 -> 319[label="",style="solid", color="burlywood", weight=3];
420[label="wu24/True",fontsize=10,color="white",style="solid",shape="box"];301 -> 420[label="",style="solid", color="burlywood", weight=9];
420 -> 320[label="",style="solid", color="burlywood", weight=3];
305[label="wu16 == wu190\n  Eq a  Eq b",fontsize=16,color="black",shape="triangle"];305 -> 321[label="",style="solid", color="black", weight=3];
306[label="wu16 == wu190\n  Integral a",fontsize=16,color="black",shape="triangle"];306 -> 322[label="",style="solid", color="black", weight=3];
307[label="wu16 == wu190\n  Eq a  Eq b  Eq c",fontsize=16,color="black",shape="triangle"];307 -> 323[label="",style="solid", color="black", weight=3];
308[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];308 -> 324[label="",style="solid", color="black", weight=3];
309[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];309 -> 325[label="",style="solid", color="black", weight=3];
310[label="wu16 == wu190\n  Eq a  Eq b",fontsize=16,color="black",shape="triangle"];310 -> 326[label="",style="solid", color="black", weight=3];
311[label="wu16 == wu190\n  Eq a",fontsize=16,color="black",shape="triangle"];311 -> 327[label="",style="solid", color="black", weight=3];
312[label="wu16 == wu190",fontsize=16,color="burlywood",shape="triangle"];421[label="wu16/()",fontsize=10,color="white",style="solid",shape="box"];312 -> 421[label="",style="solid", color="burlywood", weight=9];
421 -> 328[label="",style="solid", color="burlywood", weight=3];
313[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];313 -> 329[label="",style="solid", color="black", weight=3];
314[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];314 -> 330[label="",style="solid", color="black", weight=3];
315[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];315 -> 331[label="",style="solid", color="black", weight=3];
316[label="wu16 == wu190\n  Eq a",fontsize=16,color="black",shape="triangle"];316 -> 332[label="",style="solid", color="black", weight=3];
317[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];317 -> 333[label="",style="solid", color="black", weight=3];
318[label="wu16 == wu190",fontsize=16,color="black",shape="triangle"];318 -> 334[label="",style="solid", color="black", weight=3];
319[label="False && isPrefixOf wu25 wu26\n  Eq a",fontsize=16,color="black",shape="box"];319 -> 335[label="",style="solid", color="black", weight=3];
320[label="True && isPrefixOf wu25 wu26\n  Eq a",fontsize=16,color="black",shape="box"];320 -> 336[label="",style="solid", color="black", weight=3];
321[label="error []",fontsize=16,color="red",shape="box"];322[label="error []",fontsize=16,color="red",shape="box"];323[label="error []",fontsize=16,color="red",shape="box"];324[label="error []",fontsize=16,color="red",shape="box"];325[label="error []",fontsize=16,color="red",shape="box"];326[label="error []",fontsize=16,color="red",shape="box"];327[label="error []",fontsize=16,color="red",shape="box"];328[label="() == wu190",fontsize=16,color="burlywood",shape="box"];422[label="wu190/()",fontsize=10,color="white",style="solid",shape="box"];328 -> 422[label="",style="solid", color="burlywood", weight=9];
422 -> 337[label="",style="solid", color="burlywood", weight=3];
329[label="error []",fontsize=16,color="red",shape="box"];330[label="error []",fontsize=16,color="red",shape="box"];331[label="error []",fontsize=16,color="red",shape="box"];332[label="error []",fontsize=16,color="red",shape="box"];333[label="error []",fontsize=16,color="red",shape="box"];334[label="error []",fontsize=16,color="red",shape="box"];335[label="False",fontsize=16,color="green",shape="box"];336[label="isPrefixOf wu25 wu26\n  Eq a",fontsize=16,color="burlywood",shape="box"];423[label="wu25/wu250 : wu251",fontsize=10,color="white",style="solid",shape="box"];336 -> 423[label="",style="solid", color="burlywood", weight=9];
423 -> 338[label="",style="solid", color="burlywood", weight=3];
424[label="wu25/[]",fontsize=10,color="white",style="solid",shape="box"];336 -> 424[label="",style="solid", color="burlywood", weight=9];
424 -> 339[label="",style="solid", color="burlywood", weight=3];
337[label="() == ()",fontsize=16,color="black",shape="box"];337 -> 340[label="",style="solid", color="black", weight=3];
338[label="isPrefixOf (wu250 : wu251) wu26\n  Eq a",fontsize=16,color="burlywood",shape="box"];425[label="wu26/wu260 : wu261",fontsize=10,color="white",style="solid",shape="box"];338 -> 425[label="",style="solid", color="burlywood", weight=9];
425 -> 341[label="",style="solid", color="burlywood", weight=3];
426[label="wu26/[]",fontsize=10,color="white",style="solid",shape="box"];338 -> 426[label="",style="solid", color="burlywood", weight=9];
426 -> 342[label="",style="solid", color="burlywood", weight=3];
339[label="isPrefixOf [] wu26\n  Eq a",fontsize=16,color="black",shape="box"];339 -> 343[label="",style="solid", color="black", weight=3];
340[label="True",fontsize=16,color="green",shape="box"];341[label="isPrefixOf (wu250 : wu251) (wu260 : wu261)\n  Eq a",fontsize=16,color="black",shape="box"];341 -> 344[label="",style="solid", color="black", weight=3];
342[label="isPrefixOf (wu250 : wu251) []\n  Eq a",fontsize=16,color="black",shape="box"];342 -> 345[label="",style="solid", color="black", weight=3];
343[label="True",fontsize=16,color="green",shape="box"];344 -> 301[label="",style="dashed", color="red", weight=0];
344[label="wu250 == wu260 && isPrefixOf wu251 wu261\n  Eq a",fontsize=16,color="magenta"];344 -> 346[label="",style="dashed", color="magenta", weight=3];
344 -> 347[label="",style="dashed", color="magenta", weight=3];
344 -> 348[label="",style="dashed", color="magenta", weight=3];
345[label="False",fontsize=16,color="green",shape="box"];346[label="wu250 == wu260\n  Eq a",fontsize=16,color="blue",shape="box"];428[label="== :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 428[label="",style="solid", color="blue", weight=9];
428 -> 349[label="",style="solid", color="blue", weight=3];
429[label="== :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 429[label="",style="solid", color="blue", weight=9];
429 -> 350[label="",style="solid", color="blue", weight=3];
430[label="== :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 430[label="",style="solid", color="blue", weight=9];
430 -> 351[label="",style="solid", color="blue", weight=3];
431[label="== :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 431[label="",style="solid", color="blue", weight=9];
431 -> 352[label="",style="solid", color="blue", weight=3];
432[label="== :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 432[label="",style="solid", color="blue", weight=9];
432 -> 353[label="",style="solid", color="blue", weight=3];
433[label="== :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 433[label="",style="solid", color="blue", weight=9];
433 -> 354[label="",style="solid", color="blue", weight=3];
434[label="== :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 434[label="",style="solid", color="blue", weight=9];
434 -> 355[label="",style="solid", color="blue", weight=3];
435[label="== :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 435[label="",style="solid", color="blue", weight=9];
435 -> 356[label="",style="solid", color="blue", weight=3];
436[label="== :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 436[label="",style="solid", color="blue", weight=9];
436 -> 357[label="",style="solid", color="blue", weight=3];
437[label="== :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 437[label="",style="solid", color="blue", weight=9];
437 -> 358[label="",style="solid", color="blue", weight=3];
438[label="== :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 438[label="",style="solid", color="blue", weight=9];
438 -> 359[label="",style="solid", color="blue", weight=3];
439[label="== :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 439[label="",style="solid", color="blue", weight=9];
439 -> 360[label="",style="solid", color="blue", weight=3];
440[label="== :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 440[label="",style="solid", color="blue", weight=9];
440 -> 361[label="",style="solid", color="blue", weight=3];
441[label="== :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];346 -> 441[label="",style="solid", color="blue", weight=9];
441 -> 362[label="",style="solid", color="blue", weight=3];
347[label="wu261\n  Eq a",fontsize=16,color="green",shape="box"];348[label="wu251\n  Eq a",fontsize=16,color="green",shape="box"];349 -> 305[label="",style="dashed", color="red", weight=0];
349[label="wu250 == wu260\n  Eq a  Eq b",fontsize=16,color="magenta"];349 -> 363[label="",style="dashed", color="magenta", weight=3];
349 -> 364[label="",style="dashed", color="magenta", weight=3];
350 -> 306[label="",style="dashed", color="red", weight=0];
350[label="wu250 == wu260\n  Integral a",fontsize=16,color="magenta"];350 -> 365[label="",style="dashed", color="magenta", weight=3];
350 -> 366[label="",style="dashed", color="magenta", weight=3];
351 -> 307[label="",style="dashed", color="red", weight=0];
351[label="wu250 == wu260\n  Eq a  Eq b  Eq c",fontsize=16,color="magenta"];351 -> 367[label="",style="dashed", color="magenta", weight=3];
351 -> 368[label="",style="dashed", color="magenta", weight=3];
352 -> 308[label="",style="dashed", color="red", weight=0];
352[label="wu250 == wu260",fontsize=16,color="magenta"];352 -> 369[label="",style="dashed", color="magenta", weight=3];
352 -> 370[label="",style="dashed", color="magenta", weight=3];
353 -> 309[label="",style="dashed", color="red", weight=0];
353[label="wu250 == wu260",fontsize=16,color="magenta"];353 -> 371[label="",style="dashed", color="magenta", weight=3];
353 -> 372[label="",style="dashed", color="magenta", weight=3];
354 -> 310[label="",style="dashed", color="red", weight=0];
354[label="wu250 == wu260\n  Eq a  Eq b",fontsize=16,color="magenta"];354 -> 373[label="",style="dashed", color="magenta", weight=3];
354 -> 374[label="",style="dashed", color="magenta", weight=3];
355 -> 311[label="",style="dashed", color="red", weight=0];
355[label="wu250 == wu260\n  Eq a",fontsize=16,color="magenta"];355 -> 375[label="",style="dashed", color="magenta", weight=3];
355 -> 376[label="",style="dashed", color="magenta", weight=3];
356 -> 312[label="",style="dashed", color="red", weight=0];
356[label="wu250 == wu260",fontsize=16,color="magenta"];356 -> 377[label="",style="dashed", color="magenta", weight=3];
356 -> 378[label="",style="dashed", color="magenta", weight=3];
357 -> 313[label="",style="dashed", color="red", weight=0];
357[label="wu250 == wu260",fontsize=16,color="magenta"];357 -> 379[label="",style="dashed", color="magenta", weight=3];
357 -> 380[label="",style="dashed", color="magenta", weight=3];
358 -> 314[label="",style="dashed", color="red", weight=0];
358[label="wu250 == wu260",fontsize=16,color="magenta"];358 -> 381[label="",style="dashed", color="magenta", weight=3];
358 -> 382[label="",style="dashed", color="magenta", weight=3];
359 -> 315[label="",style="dashed", color="red", weight=0];
359[label="wu250 == wu260",fontsize=16,color="magenta"];359 -> 383[label="",style="dashed", color="magenta", weight=3];
359 -> 384[label="",style="dashed", color="magenta", weight=3];
360 -> 316[label="",style="dashed", color="red", weight=0];
360[label="wu250 == wu260\n  Eq a",fontsize=16,color="magenta"];360 -> 385[label="",style="dashed", color="magenta", weight=3];
360 -> 386[label="",style="dashed", color="magenta", weight=3];
361 -> 317[label="",style="dashed", color="red", weight=0];
361[label="wu250 == wu260",fontsize=16,color="magenta"];361 -> 387[label="",style="dashed", color="magenta", weight=3];
361 -> 388[label="",style="dashed", color="magenta", weight=3];
362 -> 318[label="",style="dashed", color="red", weight=0];
362[label="wu250 == wu260",fontsize=16,color="magenta"];362 -> 389[label="",style="dashed", color="magenta", weight=3];
362 -> 390[label="",style="dashed", color="magenta", weight=3];
363[label="wu250\n  Eq a  Eq b",fontsize=16,color="green",shape="box"];364[label="wu260\n  Eq a  Eq b",fontsize=16,color="green",shape="box"];365[label="wu250\n  Integral a",fontsize=16,color="green",shape="box"];366[label="wu260\n  Integral a",fontsize=16,color="green",shape="box"];367[label="wu250\n  Eq a  Eq b  Eq c",fontsize=16,color="green",shape="box"];368[label="wu260\n  Eq a  Eq b  Eq c",fontsize=16,color="green",shape="box"];369[label="wu250",fontsize=16,color="green",shape="box"];370[label="wu260",fontsize=16,color="green",shape="box"];371[label="wu250",fontsize=16,color="green",shape="box"];372[label="wu260",fontsize=16,color="green",shape="box"];373[label="wu250\n  Eq a  Eq b",fontsize=16,color="green",shape="box"];374[label="wu260\n  Eq a  Eq b",fontsize=16,color="green",shape="box"];375[label="wu250\n  Eq a",fontsize=16,color="green",shape="box"];376[label="wu260\n  Eq a",fontsize=16,color="green",shape="box"];377[label="wu250",fontsize=16,color="green",shape="box"];378[label="wu260",fontsize=16,color="green",shape="box"];379[label="wu250",fontsize=16,color="green",shape="box"];380[label="wu260",fontsize=16,color="green",shape="box"];381[label="wu250",fontsize=16,color="green",shape="box"];382[label="wu260",fontsize=16,color="green",shape="box"];383[label="wu250",fontsize=16,color="green",shape="box"];384[label="wu260",fontsize=16,color="green",shape="box"];385[label="wu250\n  Eq a",fontsize=16,color="green",shape="box"];386[label="wu260\n  Eq a",fontsize=16,color="green",shape="box"];387[label="wu250",fontsize=16,color="green",shape="box"];388[label="wu260",fontsize=16,color="green",shape="box"];389[label="wu250",fontsize=16,color="green",shape="box"];390[label="wu260",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_asAs(True, :(wu250, wu251), :(wu260, wu261), ba) → new_asAs(new_esEs(wu250, wu260, ba), wu251, wu261, ba)

The TRS R consists of the following rules:

new_esEs(wu250, wu260, ty_Char) → new_esEs7(wu250, wu260)
new_esEs11(wu16, wu190, dc, dd) → error([])
new_esEs(wu250, wu260, ty_Double) → new_esEs9(wu250, wu260)
new_esEs(wu250, wu260, ty_Integer) → new_esEs4(wu250, wu260)
new_esEs(wu250, wu260, ty_Int) → new_esEs13(wu250, wu260)
new_esEs7(wu16, wu190) → error([])
new_esEs(wu250, wu260, app(ty_Maybe, db)) → new_esEs6(wu250, wu260, db)
new_esEs(wu250, wu260, app(ty_Ratio, cb)) → new_esEs3(wu250, wu260, cb)
new_esEs3(wu16, wu190, bc) → error([])
new_esEs(wu250, wu260, app(app(ty_Either, cf), cg)) → new_esEs12(wu250, wu260, cf, cg)
new_esEs4(wu16, wu190) → error([])
new_esEs6(wu16, wu190, bd) → error([])
new_esEs(wu250, wu260, ty_Float) → new_esEs10(wu250, wu260)
new_esEs8(wu16, wu190, be, bf, bg) → error([])
new_esEs13(wu16, wu190) → error([])
new_esEs(wu250, wu260, ty_Ordering) → new_esEs1(wu250, wu260)
new_esEs(wu250, wu260, app(ty_[], da)) → new_esEs2(wu250, wu260, da)
new_esEs9(wu16, wu190) → error([])
new_esEs(wu250, wu260, app(app(ty_@2, bh), ca)) → new_esEs11(wu250, wu260, bh, ca)
new_esEs(wu250, wu260, ty_@0) → new_esEs5(wu250, wu260)
new_esEs1(wu16, wu190) → error([])
new_esEs12(wu16, wu190, de, df) → error([])
new_esEs5(@0, @0) → True
new_esEs10(wu16, wu190) → error([])
new_esEs2(wu16, wu190, bb) → error([])
new_esEs(wu250, wu260, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(wu250, wu260, cc, cd, ce)
new_esEs0(wu16, wu190) → error([])
new_esEs(wu250, wu260, ty_Bool) → new_esEs0(wu250, wu260)

The set Q consists of the following terms:

new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs1(x0, x1)
new_esEs6(x0, x1, x2)
new_esEs4(x0, x1)
new_esEs13(x0, x1)
new_esEs9(x0, x1)
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, ty_Char)
new_esEs5(@0, @0)
new_esEs11(x0, x1, x2, x3)
new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs2(x0, x1, x2)
new_esEs(x0, x1, app(ty_[], x2))
new_esEs12(x0, x1, x2, x3)
new_esEs0(x0, x1)
new_esEs(x0, x1, ty_Ordering)
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1)
new_esEs8(x0, x1, x2, x3, x4)
new_esEs(x0, x1, ty_Int)
new_esEs(x0, x1, ty_Double)
new_esEs3(x0, x1, x2)
new_esEs7(x0, x1)
new_esEs(x0, x1, ty_@0)
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, app(app(ty_Either, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_asAs(True, :(wu250, wu251), :(wu260, wu261), ba) → new_asAs(new_esEs(wu250, wu260, ba), wu251, wu261, ba)
The graph contains the following edges 2 > 2, 3 > 3, 4 >= 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(wu16, wu15, wu19, :(wu1810, wu1811), ba) → new_isPrefixOf(wu16, wu15, new_flip(wu19, wu1810, ba), wu1811, ba)

The TRS R consists of the following rules:

new_flip(wu15, wu16, ba) → :(wu16, wu15)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_isPrefixOf(wu16, wu15, wu19, :(wu1810, wu1811), ba) → new_isPrefixOf(wu16, wu15, new_flip(wu19, wu1810, ba), wu1811, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf0(wu15, wu16, :(wu170, wu171), wu18, ba) → new_isPrefixOf0(new_flip(wu15, wu16, ba), wu170, wu171, wu18, ba)

The TRS R consists of the following rules:

new_flip(wu15, wu16, ba) → :(wu16, wu15)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_isPrefixOf0(wu15, wu16, :(wu170, wu171), wu18, ba) → new_isPrefixOf0(new_flip(wu15, wu16, ba), wu170, wu171, wu18, ba)
The graph contains the following edges 3 > 2, 3 > 3, 4 >= 4, 5 >= 5